YES 0.919 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule List
  ((tails :: [a ->  [[a]]) :: [a ->  [[a]])

module List where
  import qualified Maybe
import qualified Prelude

  tails :: [a ->  [[a]]
tails [] [] : []
tails xxs@(_ : xsxxs : tails xs


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xxs@(vx : vy)

is replaced by the following term
vx : vy



↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule List
  ((tails :: [a ->  [[a]]) :: [a ->  [[a]])

module List where
  import qualified Maybe
import qualified Prelude

  tails :: [a ->  [[a]]
tails [] [] : []
tails (vx : vy(vx : vy: tails vy


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule List
  (tails :: [a ->  [[a]])

module List where
  import qualified Maybe
import qualified Prelude

  tails :: [a ->  [[a]]
tails [] [] : []
tails (vx : vy(vx : vy: tails vy


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
QDP
              ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_tails(:(wv30, wv31), ba) → new_tails(wv31, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: